fpf-compatible(A; a.B(a); eq; f; g)
== x:A. 
== ((fpf-dom(eq; x; f))  (fpf-dom(eq; x; g)))  (fpf-ap(f; eq; x) = fpf-ap(g; eq; x)) 

latex

---

clarification:

fpf-compatible(A; a.B(a); eq; f; g)
== x:A. 
== ((fpf-dom(eq; x; f))  (fpf-dom(eq; x; g)))
==  (fpf-ap(f; eq; x) = fpf-ap(g; eq; x)  B(x)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, b, fpf-dom(eq; x; f), fpf-ap(f; eq; x)
FDL editor aliases	fpf-compatible